Nuprl Definition : ma-send 0,22

M.send(k;l;s;v;ms;i)
== L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>)
== 
== ms = if source(l) = i concat(map(tgf.map(x.<1of(tgf),x>;2of(tgf)(s,v));L)) else nil fi 
latex



clarification:

M.send(k;l;s;v;ms;i)
== fpf-val(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);
== fpf-val(1of(2of(2of(2of(2of(2of(M))))));
== fpf-val(<k,l>;
== fpf-val(k,L.(ms
== fpf-val(k,L.(=
== fpf-val(k,L.(if source(l) = i concat(map(tgf.map(x.<1of(tgf),x>;2of(tgf)(s,v));L)) else nil fi
== fpf-val(k,L.( (tg:Idif source(l) = i M.da(rcv(l,tg)) else Top fi) List)) 
latex


Definitionsz != f(x P(a;z), product-deq(A;B;a;b), Knd, IdLnk, KindDeq, IdLnkDeq, s = t, type List, x:AB(x), Id, M.da(a), rcv(l,tg), Top, if b t else f fi, a = b, source(l), concat(ll), map(f;as), x.A(x), <a,b>, 1of(t), f(a), 2of(t), nil
FDL editor aliasesma-send

origin